FDL - Step of Proof: less-fast-fib

Step of Proof: less-fast-fib

Inference at * 2
Iof proof for Lemma less-fast-fib:

1.

n, a, b:

.
1. {m:

|
1. {

k:

. (a = fib(k))

((k

0)

(b = 0))

((0 < k)

(b = fib(k - 1)))

(m = fib(n+k))}

n:

. {m:

| m = fib(n)}

by RenameVar `f' 1

1:

1: 1.

n, a, b:

.

1: 1. {m:

|

1: 1. {

k:

.

1: 1. {(a = fib(k))

((k

0)

(b = 0))

((0 < k)

(b = fib(k - 1)))

(m = fib(n+k))}

1:

n:

. {m:

| m = fib(n)}

.